FDL - Nuprl Definition : weak-antecedent-function

Nuprl Definition : weak-antecedent-function

11,40

==f== P ==

e:{e:E| P(e)} . f(e) c

e & Q(f(e))

clarification:

weak-antecedent-function(es;P;Q;f) ==

e:{e:es-E(es)| P(e)} . es-causle(es;f(e);e) & Q(f(e))

Definitions x:A. B(x), {x:A| B(x)} , E, P & Q, e c e', f(a)

FDL editor aliases weak-antecedent-function

Definitions	x:A. B(x), {x:A\| B(x)} , E, P & Q, e c e', f(a)
FDL editor aliases	weak-antecedent-function